\documentclass{beamer}

% \usepackage{beamerthemesplit} % Activate for custom appearance
\usepackage{k}

\title{PhD First Year Report}
\author{Andrei Arusoaie}
\date{\today}

\nonstopmode
\begin{document}

\frame{\titlepage}

\section[Outline]{}
\frame{\tableofcontents}

\section{Introduction}

\frame{
	\frametitle{PhD Program}
	\begin{itemize}
	\item PhD Student: Andrei Arusoaie
	\item Supervisor: Prof. Dr. Dorel Lucanu
	\item Co-supervisor: Dr. Vlad Rusu
	\item Duration: $\geq$ 3 years (hopefully =)
	\item Started: 1$^{st}$ of October, 2011
	\end{itemize}
}

\subsection{Initial goal}
\frame{
	\frametitle{Initial goal - Object Constraint Language Semantics}
	\begin{itemize}
	\item<1-> There was a \K semantics of OCL ...
	\item<2-> ... implementing the {\it static} part of OCL
	\item<3-> Goal: {\it dynamic} OCL
	\item<4-> Execute methods using pre/post conditions
	\item<5-> Use it in MDE (Model Driven Engineering)
	\end{itemize}
}

\subsection{Current goal}
\frame{
	\frametitle{From initial goal to symbolic execution}
	\begin{itemize}
	\item<1-> Pre/post conditions: boolean expressions over class attributes
	\item<2-> Attributes = symbolic values
	\item<3-> {\tt syntax Int ::= "symInt" "(" Int ")"}
	\item<4-> Why not adding symbolic values as builtin in \K ?
	\item<5-> Why not having generic symbolic execution support in \K?
	\end{itemize}
}

\frame{
	\frametitle{Current goal}
	\begin{itemize}
	\item Symbolic execution in the \K Framework with Applications	
	\end{itemize}
}

\frame{
	\frametitle{Motivation}
	\begin{itemize}
	\item<1-> generic symbolic execution
	\item<2-> based on formal semantics
	\item<3-> clear distinction between language independent and language specific aspects regarding symbolic execution
	\end{itemize}
}

\section{Research description}
\subsection{Symbolic execution}

\frame{
	\frametitle{Symbolic execution}
	What is symbolic execution?
	\begin{itemize}
	\item Use symbolic values instead of actual data
	\item Execution = manipulating program expressions involving symbolic values
	\item Allows reasoning about multiple concrete executions
	\end{itemize}
}

\subsection{Main goals}
\frame{
	\frametitle{Main goals}
	\begin{enumerate}
	\item<1-> Support for symbolic execution in \K
	\item<2-> Applications of symbolic execution
	\item<3-> Deductive systems over \K symbolic executions
	\end{enumerate}
}

\subsection{Proposed approach}
\frame{
	\frametitle{Proposed approach}
	\begin{itemize}
	\item Add symbolic values to \K builtin types
	\item Investigate applications for symbolic execution
	\end{itemize}
}

\section{Progress report}
\subsection{Main achievements}
\frame{
	\frametitle{Main achievements}
	\begin{itemize}
	\item<1-> OCL semantics: pre/post conditions
	\item<2-> Symbolic values: Bool, Int
	\item<3-> Connection to SMT solver
	\item<4-> IMP applications
	\end{itemize}
}

\subsection{Symbolic execution - IMP example}
\frame{
\frametitle{Find minimum}
\begin{itemize}
\item Find minimum from {\tt a}, {\tt b}, and {\tt c}:\\
\vspace{1cm}
% \item 
\begin{minipage}{.2\linewidth}
\ttfamily
\selectfont
\begin{tabular}[t]{l l l}
var a, b, c, min;&&\\
if ( a <= b )&&\\
&\hspace{-8.5cm}then if (a <= c)&\\
&&\hspace{-7.5cm}then min := a\\
&&\hspace{-7.5cm}else min := b\\
&&\hspace{-7.5cm}// else min := c\\
&\hspace{-8.5cm}else if (b <= c)&\\
&&\hspace{-7.5cm}then min := b\\
&&\hspace{-7.5cm}else min := c;\\
assert(min <= a and min <= b and min <= c)&&\\
\end{tabular}
\end{minipage}
\end{itemize}

}

\frame{
\frametitle{Find minimum}
\begin{itemize}
\item Expressions:\\\\
\vspace{1cm}
\begin{minipage}{.7\linewidth}
\ttfamily
\fontsize{9}{10}
\selectfont
\hspace{-0.7cm}
\begin{tabular}{ l || r }
\hline \hline
symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) $\leq$ symInt(c) & true \\
\hline
symInt(a) $>$ symInt(b) $\wedge$ symInt(b) $\leq$ symInt(c) & true \\
\hline
symInt(a) $>$ symInt(b) $\wedge$ symInt(b) > symInt(c) & true \\
\hline
symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) > symInt(c) 
%$\wedge$ symInt(b) $\leq$ symInt(a) 
& false \\
%\hline
%symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) > symInt(c) $\wedge$ symInt(b) > symInt(a) & false \\
\hline \hline
\end{tabular}\\\\
\end{minipage}
\end{itemize}

}

\subsection{Research papers}
\frame{
	\frametitle{Research papers and publications}
	\begin{itemize}
	\item K'11: {\it The K Primer (version 2.5)}, {\it Towards a \K semantics of OCL}
	\item WRLA'12: {\it Making Maude Definitions more Interactive}
	\item FM'12: {\it Executing Formal Semantics with the K Tool}
	\item SYNASC'12: {\it Automating Abstract Syntax Tree construction for
Context Free Grammars}
	\end{itemize}
}

\section{Future work}
\frame{
	\frametitle{Future work}
	\begin{itemize}
	\item<1-> Formal background
	\item<2-> Improving the implementation
	\item<3-> Find new features to add to symbolic execution
	\item<4-> Applications
	\item<5-> Deductive systems
	\end{itemize}
}

\end{document}
